; <lemma>
;  <title>ch915_bin.2</title>
;  <origin>ch915_bin | bin_m1 | INITIALISATION/act3/FIS</origin>
(benchmark ch915_bin_2
;  <theories>
;    <theory name="linear_order_int"/>
;    <theory name="basic_set"/>
;  </theories>
  :logic AUFLIA
;  <typenv>
;    <variable name="n" type="INTEGER"/>
;  </typenv>
  :extrafuns ((n Int))
  :extramacros (
		 (range (lambda (?i1 Int) (?i2 Int) .
			  (lambda (?i Int) .
			    (and (<= ?i1 ?i) (<= ?i ?i2)))))
		 (emptyset (lambda (?x 't). false))
		 )
; <hypothesis needed="true">n >= 1</hypothesis>
  :assumption (>= n 1)
; <goal>not 1 .. n = {}</goal>
  :formula
  (not
      (not (= (range 1 n) emptyset))
    )
)
; </lemma>

